Nuprl Lemma : rel_plus_wf
0,22
postcript
pdf
T
:Type,
R
:(
T
T
Type).
R
^+
T
T
Type
latex
Definitions
R
^+
,
x
:
A
.
B
(
x
)
,
,
x
f
y
,
rel_exp(
T
;
R
;
n
)
,
x
:
A
.
B
(
x
)
,
Prop
,
t
T
Lemmas
nat
plus
inc
,
rel
exp
wf
,
nat
plus
wf
origin
T:Type, R:(T
TType). R^+ 
TTType T:Type, R:(TTType). R^+ TTType 
x:A. B(x)
x:A. B(x) T